$\forall$$T$:Type, $L$:(($T$$\rightarrow\mathbb{P}$) List), $P$:($T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$Q$$\in$$L$. $\forall$$x$:$T$. Dec($Q$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$Q$$\in$$L$. finite{-}type(\{$x$:$T$$\mid$ $Q$($x$)\} ))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$. $P$($x$) $\Rightarrow$ ($\exists$$Q$$\in$$L$.$Q$($x$)))
\\[0ex]$\Rightarrow$ finite{-}type(\{$x$:$T$$\mid$ $P$($x$)\} )